Nuprl Lemma : fpf-dom-type2
0,22
postcript
pdf
X
,
Y
:Type,
eq
:EqDecider(
Y
),
f
:
x
:
X
fp
Top,
x
:
Y
. strong-subtype(
X
;
Y
)
{
x
dom(
f
)
x
X
}
latex
Definitions
{
T
}
Lemmas
fpf-dom-type
origin
X, Y:Type, eq:EqDecider(Y), f:x:X fp
Top, x:Y. strong-subtype(X;Y) 
{x 
dom(f) x X} X, Y:Type, eq:EqDecider(Y), f:x:X fp Top, x:Y. strong-subtype(X;Y) {x dom(f) x X}